A:Type, l:(A List). ((l = []))  ge(||l||; 1) 

latex

Definitions	t  T, x:A. B(x), prop{i:l}, P  Q, Y, ||as||, False, A  B, ge(i; j), A
Lemmas	not wf, length wf1, non neg length